(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Hanoi
public class Hanoi {
private void solve(int h, int from, int to, int support) {
if (h < 1) return;
else if (h == 1) {
//System.out.println("from " + from + " to " + to + "\n");
}
else {
solve(h - 1, from, support, to);
//System.out.println("from " + from + " to " + to + "\n");
solve(h - 1, support, to, from);
}
}

public static void main(String[] args) {
new Hanoi().solve(5,1,2,3);
}
}


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Hanoi.main([Ljava/lang/String;)V: Graph of 488 nodes with 0 SCCs.


(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

(4) TRUE